M1, M2:MsgA. M1 || M2  M2 || M1 

latex

Definitions	x:A. B(x), P  Q, M1 || M2, 1of(t), 2of(t), M1 ||decl M2, t  T, f  g, A & B, x. t(x), Prop, P  Q, b, True, true, {T}, if b t else f fi, P  Q, P  Q, P & Q, false, MsgA, Valtype(da;k), x(s), Dec(P), False, A, SQType(T), , Unit, f || g,
Lemmas	ma-compatible wf, msga wf, assert wf, fpf-dom wf, Id wf, id-deq wf, fpf-join wf, top wf, fpf-trivial-subtype-top, fpf-join-dom, fpf wf, decidable or, decidable assert, assert elim, bool sq, fpf-join-ap, bool wf, eqtt to assert, iff transitivity, bnot wf, not wf, eqff to assert, assert of bnot, fpf-ap wf, Knd wf, Kind-deq wf